g:IMonoid, n:. (n  e) = e  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, n x(op;id) e, n  e
Definitions	t  T, x:A. B(x), False, A, A  B, P  Q, n x(op;id) e, n  e, P & Q, x. t(x), P  Q, P  Q, , IMonoid, x(s),
Lemmas	imon wf, nat wf, le wf, grp id wf, mon nat op zero, grp op wf, itop wf, mon ident, int seg wf, itop unroll hi, grp car wf